Left Termination proof of /tmp/tmpggJNEA/inorder-oi.pl

Left Termination of the query pattern
in_order(a,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇒, 586 ms)

↳2 TRIPLES

↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)

↳4 TRIPLES

↳5 TriplesToPiDPProof (⇒, 189 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇒, 1 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇒, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

    ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 52 ms)

        ↳25 QDP

        ↳26 QDPOrderProof (⇔, 3345 ms)

        ↳27 QDP

        ↳28 DependencyGraphProof (⇔, 0 ms)

        ↳29 QDP

        ↳30 UsableRulesProof (⇔, 0 ms)

        ↳31 QDP

        ↳32 QReductionProof (⇔, 0 ms)

        ↳33 QDP

        ↳34 QDPQMonotonicMRRProof (⇔, 622 ms)

        ↳35 QDP

        ↳36 QDPOrderProof (⇔, 1032 ms)

        ↳37 QDP

        ↳38 DependencyGraphProof (⇔, 0 ms)

        ↳39 TRUE

(0) Obligation:

Clauses:

in_order(void, L) :- ','(!, eq(L, [])).
in_order(T, Xs) :- ','(value(T, X), ','(app(Ls, .(X, Rs), Xs), ','(left(T, L), ','(in_order(L, Ls), ','(right(T, R), in_order(R, Rs)))))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
left(void, void).
left(node(L, X1, X2), L).
right(void, void).
right(node(X3, X4, R), R).
value(void, X5).
value(node(X6, X, X7), X).
eq(X, X).

Query: in_order(a,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="D: in_order(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: in_order(T1, T2), SCOPE: 1, CLAUSE: 0 | in_order(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(!_1, eq(T4, [])) | in_order(T1, T4), SCOPE: 1, CLAUSE: 1\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: in_order(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX9 is free\nin_order(T1, T2) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: eq(T4, [])\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: eq(T4, []), SCOPE: 2, CLAUSE: 10\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19))))))\n\nT11 is ground\nX9 is free\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19)))))), SCOPE: 3, CLAUSE: 8 | ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19)))))), SCOPE: 3, CLAUSE: 9\n\nT11 is ground\nX9 is free\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19)))))), SCOPE: 3, CLAUSE: 8\n\nT11 is ground\nX9 is free\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19)))))), SCOPE: 3, CLAUSE: 9\n\nT11 is ground\nX9 is free\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(app(X18, .(X31, X19), T11), ','(left(void, X20), ','(in_order(X20, X18), ','(right(void, X21), in_order(X21, X19)))))\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="E: app(X18, .(X31, X19), T11)\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19))))\n\nT17 is ground\nT19 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: app(X18, .(X31, X19), T11), SCOPE: 4, CLAUSE: 2 | app(X18, .(X31, X19), T11), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: app(X18, .(X31, X19), T11), SCOPE: 4, CLAUSE: 2\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: app(X18, .(X31, X19), T11), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: app(X80, .(X81, X82), T39)\n\nT38 is ground\nT39 is ground\nX9 is free\nX80 is free\nX81 is free\nX82 is free\nin_order(T1, .(T38, T39)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: app(X80, .(X81, X82), T39), SCOPE: 5, CLAUSE: 2 | app(X80, .(X81, X82), T39), SCOPE: 5, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nX9 is free\nX80 is free\nX81 is free\nX82 is free\nin_order(T1, .(T38, T39)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: app(X80, .(X81, X82), T39), SCOPE: 5, CLAUSE: 2\n\nT38 is ground\nT39 is ground\nX9 is free\nX80 is free\nX81 is free\nX82 is free\nin_order(T1, .(T38, T39)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: app(X80, .(X81, X82), T39), SCOPE: 5, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nX9 is free\nX80 is free\nX81 is free\nX82 is free\nin_order(T1, .(T38, T39)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: app(X125, .(X126, X127), T59)\n\nT38 is ground\nT58 is ground\nT59 is ground\nX9 is free\nX125 is free\nX126 is free\nX127 is free\nin_order(T1, .(T38, .(T58, T59))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: app(X125, .(X126, X127), T59), SCOPE: 6, CLAUSE: 2 | app(X125, .(X126, X127), T59), SCOPE: 6, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT59 is ground\nX9 is free\nX125 is free\nX126 is free\nX127 is free\nin_order(T1, .(T38, .(T58, T59))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: app(X125, .(X126, X127), T59), SCOPE: 6, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT59 is ground\nX9 is free\nX125 is free\nX126 is free\nX127 is free\nin_order(T1, .(T38, .(T58, T59))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: app(X125, .(X126, X127), T59), SCOPE: 6, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT59 is ground\nX9 is free\nX125 is free\nX126 is free\nX127 is free\nin_order(T1, .(T38, .(T58, T59))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: app(X170, .(X171, X172), T79)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT79 is ground\nX9 is free\nX170 is free\nX171 is free\nX172 is free\nin_order(T1, .(T38, .(T58, .(T78, T79)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: app(X170, .(X171, X172), T79), SCOPE: 7, CLAUSE: 2 | app(X170, .(X171, X172), T79), SCOPE: 7, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT79 is ground\nX9 is free\nX170 is free\nX171 is free\nX172 is free\nin_order(T1, .(T38, .(T58, .(T78, T79)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: app(X170, .(X171, X172), T79), SCOPE: 7, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT79 is ground\nX9 is free\nX170 is free\nX171 is free\nX172 is free\nin_order(T1, .(T38, .(T58, .(T78, T79)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: app(X170, .(X171, X172), T79), SCOPE: 7, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT79 is ground\nX9 is free\nX170 is free\nX171 is free\nX172 is free\nin_order(T1, .(T38, .(T58, .(T78, T79)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: app(X215, .(X216, X217), T99)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT99 is ground\nX9 is free\nX215 is free\nX216 is free\nX217 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, T99))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: app(X215, .(X216, X217), T99), SCOPE: 8, CLAUSE: 2 | app(X215, .(X216, X217), T99), SCOPE: 8, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT99 is ground\nX9 is free\nX215 is free\nX216 is free\nX217 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, T99))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: app(X215, .(X216, X217), T99), SCOPE: 8, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT99 is ground\nX9 is free\nX215 is free\nX216 is free\nX217 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, T99))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: app(X215, .(X216, X217), T99), SCOPE: 8, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT99 is ground\nX9 is free\nX215 is free\nX216 is free\nX217 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, T99))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: app(X260, .(X261, X262), T119)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT119 is ground\nX9 is free\nX260 is free\nX261 is free\nX262 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, T119)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: app(X260, .(X261, X262), T119), SCOPE: 9, CLAUSE: 2 | app(X260, .(X261, X262), T119), SCOPE: 9, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT119 is ground\nX9 is free\nX260 is free\nX261 is free\nX262 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, T119)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: app(X260, .(X261, X262), T119), SCOPE: 9, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT119 is ground\nX9 is free\nX260 is free\nX261 is free\nX262 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, T119)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: app(X260, .(X261, X262), T119), SCOPE: 9, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT119 is ground\nX9 is free\nX260 is free\nX261 is free\nX262 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, T119)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: app(X305, .(X306, X307), T139)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT139 is ground\nX9 is free\nX305 is free\nX306 is free\nX307 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, T139))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: app(X305, .(X306, X307), T139), SCOPE: 10, CLAUSE: 2 | app(X305, .(X306, X307), T139), SCOPE: 10, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT139 is ground\nX9 is free\nX305 is free\nX306 is free\nX307 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, T139))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: app(X305, .(X306, X307), T139), SCOPE: 10, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT139 is ground\nX9 is free\nX305 is free\nX306 is free\nX307 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, T139))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: app(X305, .(X306, X307), T139), SCOPE: 10, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT139 is ground\nX9 is free\nX305 is free\nX306 is free\nX307 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, T139))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: app(X350, .(X351, X352), T159)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT159 is ground\nX9 is free\nX350 is free\nX351 is free\nX352 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, T159)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: app(X350, .(X351, X352), T159), SCOPE: 11, CLAUSE: 2 | app(X350, .(X351, X352), T159), SCOPE: 11, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT159 is ground\nX9 is free\nX350 is free\nX351 is free\nX352 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, T159)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: app(X350, .(X351, X352), T159), SCOPE: 11, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT159 is ground\nX9 is free\nX350 is free\nX351 is free\nX352 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, T159)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: app(X350, .(X351, X352), T159), SCOPE: 11, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT159 is ground\nX9 is free\nX350 is free\nX351 is free\nX352 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, T159)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: app(X395, .(X396, X397), T179)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT178 is ground\nT179 is ground\nX9 is free\nX395 is free\nX396 is free\nX397 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="A: app(X395, .(X396, X397), T179)\n\nT179 is ground\nX395 is free\nX396 is free\nX397 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: app(X395, .(X396, X397), T179), SCOPE: 12, CLAUSE: 2 | app(X395, .(X396, X397), T179), SCOPE: 12, CLAUSE: 3\n\nT179 is ground\nX395 is free\nX396 is free\nX397 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: app(X395, .(X396, X397), T179), SCOPE: 12, CLAUSE: 2\n\nT179 is ground\nX395 is free\nX396 is free\nX397 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: app(X395, .(X396, X397), T179), SCOPE: 12, CLAUSE: 3\n\nT179 is ground\nX395 is free\nX396 is free\nX397 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: app(X446, .(X447, X448), T204)\n\nT204 is ground\nX446 is free\nX447 is free\nX448 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19)))), SCOPE: 13, CLAUSE: 4 | ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19)))), SCOPE: 13, CLAUSE: 5\n\nT17 is ground\nT19 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19)))), SCOPE: 13, CLAUSE: 4\n\nT17 is ground\nT19 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19)))), SCOPE: 13, CLAUSE: 5\n\nT17 is ground\nT19 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(in_order(void, T17), ','(right(void, X21), in_order(X21, T19)))\n\nT17 is ground\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="B: in_order(void, T17)\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(right(void, X21), in_order(X21, T19))\n\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: in_order(void, T17), SCOPE: 14, CLAUSE: 0 | in_order(void, T17), SCOPE: 14, CLAUSE: 1\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(!_14, eq(T216, [])) | in_order(void, T216), SCOPE: 14, CLAUSE: 1\n\nT216 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: eq(T216, [])\n\nT216 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: eq(T216, []), SCOPE: 15, CLAUSE: 10\n\nT216 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(right(void, X21), in_order(X21, T19)), SCOPE: 16, CLAUSE: 6 | ','(right(void, X21), in_order(X21, T19)), SCOPE: 16, CLAUSE: 7\n\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(right(void, X21), in_order(X21, T19)), SCOPE: 16, CLAUSE: 6\n\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(right(void, X21), in_order(X21, T19)), SCOPE: 16, CLAUSE: 7\n\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: in_order(void, T19)\n\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(app(X18, .(T233, X19), T11), ','(left(node(T234, T233, T235), X20), ','(in_order(X20, X18), ','(right(node(T234, T233, T235), X21), in_order(X21, X19)))))\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="F: app(X18, .(T233, X19), T11)\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(left(node(T242, T243, T244), X20), ','(in_order(X20, T240), ','(right(node(T242, T243, T244), X21), in_order(X21, T241))))\n\nT240 is ground\nT243 is ground\nT241 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: app(X18, .(T233, X19), T11), SCOPE: 17, CLAUSE: 2 | app(X18, .(T233, X19), T11), SCOPE: 17, CLAUSE: 3\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: app(X18, .(T233, X19), T11), SCOPE: 17, CLAUSE: 2\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: app(X18, .(T233, X19), T11), SCOPE: 17, CLAUSE: 3\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: app(X522, .(T269, X523), T268)\n\nT267 is ground\nT268 is ground\nX9 is free\nX522 is free\nX523 is free\nin_order(T1, .(T267, T268)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: app(X522, .(T269, X523), T268), SCOPE: 18, CLAUSE: 2 | app(X522, .(T269, X523), T268), SCOPE: 18, CLAUSE: 3\n\nT267 is ground\nT268 is ground\nX9 is free\nX522 is free\nX523 is free\nin_order(T1, .(T267, T268)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: app(X522, .(T269, X523), T268), SCOPE: 18, CLAUSE: 2\n\nT267 is ground\nT268 is ground\nX9 is free\nX522 is free\nX523 is free\nin_order(T1, .(T267, T268)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: app(X522, .(T269, X523), T268), SCOPE: 18, CLAUSE: 3\n\nT267 is ground\nT268 is ground\nX9 is free\nX522 is free\nX523 is free\nin_order(T1, .(T267, T268)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: app(X557, .(T293, X558), T292)\n\nT267 is ground\nT291 is ground\nT292 is ground\nX9 is free\nX557 is free\nX558 is free\nin_order(T1, .(T267, .(T291, T292))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: app(X557, .(T293, X558), T292), SCOPE: 19, CLAUSE: 2 | app(X557, .(T293, X558), T292), SCOPE: 19, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT292 is ground\nX9 is free\nX557 is free\nX558 is free\nin_order(T1, .(T267, .(T291, T292))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: app(X557, .(T293, X558), T292), SCOPE: 19, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT292 is ground\nX9 is free\nX557 is free\nX558 is free\nin_order(T1, .(T267, .(T291, T292))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: app(X557, .(T293, X558), T292), SCOPE: 19, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT292 is ground\nX9 is free\nX557 is free\nX558 is free\nin_order(T1, .(T267, .(T291, T292))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: app(X592, .(T317, X593), T316)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT316 is ground\nX9 is free\nX592 is free\nX593 is free\nin_order(T1, .(T267, .(T291, .(T315, T316)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: app(X592, .(T317, X593), T316), SCOPE: 20, CLAUSE: 2 | app(X592, .(T317, X593), T316), SCOPE: 20, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT316 is ground\nX9 is free\nX592 is free\nX593 is free\nin_order(T1, .(T267, .(T291, .(T315, T316)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: app(X592, .(T317, X593), T316), SCOPE: 20, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT316 is ground\nX9 is free\nX592 is free\nX593 is free\nin_order(T1, .(T267, .(T291, .(T315, T316)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: app(X592, .(T317, X593), T316), SCOPE: 20, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT316 is ground\nX9 is free\nX592 is free\nX593 is free\nin_order(T1, .(T267, .(T291, .(T315, T316)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: app(X627, .(T341, X628), T340)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT340 is ground\nX9 is free\nX627 is free\nX628 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, T340))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: app(X627, .(T341, X628), T340), SCOPE: 21, CLAUSE: 2 | app(X627, .(T341, X628), T340), SCOPE: 21, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT340 is ground\nX9 is free\nX627 is free\nX628 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, T340))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: app(X627, .(T341, X628), T340), SCOPE: 21, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT340 is ground\nX9 is free\nX627 is free\nX628 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, T340))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: app(X627, .(T341, X628), T340), SCOPE: 21, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT340 is ground\nX9 is free\nX627 is free\nX628 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, T340))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: app(X662, .(T365, X663), T364)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT364 is ground\nX9 is free\nX662 is free\nX663 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, T364)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: app(X662, .(T365, X663), T364), SCOPE: 22, CLAUSE: 2 | app(X662, .(T365, X663), T364), SCOPE: 22, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT364 is ground\nX9 is free\nX662 is free\nX663 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, T364)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: app(X662, .(T365, X663), T364), SCOPE: 22, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT364 is ground\nX9 is free\nX662 is free\nX663 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, T364)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: app(X662, .(T365, X663), T364), SCOPE: 22, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT364 is ground\nX9 is free\nX662 is free\nX663 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, T364)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: app(X697, .(T389, X698), T388)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT388 is ground\nX9 is free\nX697 is free\nX698 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, T388))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: app(X697, .(T389, X698), T388), SCOPE: 23, CLAUSE: 2 | app(X697, .(T389, X698), T388), SCOPE: 23, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT388 is ground\nX9 is free\nX697 is free\nX698 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, T388))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: app(X697, .(T389, X698), T388), SCOPE: 23, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT388 is ground\nX9 is free\nX697 is free\nX698 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, T388))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: app(X697, .(T389, X698), T388), SCOPE: 23, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT388 is ground\nX9 is free\nX697 is free\nX698 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, T388))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: app(X732, .(T413, X733), T412)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT412 is ground\nX9 is free\nX732 is free\nX733 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, T412)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: app(X732, .(T413, X733), T412), SCOPE: 24, CLAUSE: 2 | app(X732, .(T413, X733), T412), SCOPE: 24, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT412 is ground\nX9 is free\nX732 is free\nX733 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, T412)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: app(X732, .(T413, X733), T412), SCOPE: 24, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT412 is ground\nX9 is free\nX732 is free\nX733 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, T412)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: app(X732, .(T413, X733), T412), SCOPE: 24, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT412 is ground\nX9 is free\nX732 is free\nX733 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, T412)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: app(X767, .(T437, X768), T436)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT435 is ground\nT436 is ground\nX9 is free\nX767 is free\nX768 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="C: app(X767, .(T437, X768), T436)\n\nT436 is ground\nX767 is free\nX768 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: app(X767, .(T437, X768), T436), SCOPE: 25, CLAUSE: 2 | app(X767, .(T437, X768), T436), SCOPE: 25, CLAUSE: 3\n\nT436 is ground\nX767 is free\nX768 is free", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: app(X767, .(T437, X768), T436), SCOPE: 25, CLAUSE: 2\n\nT436 is ground\nX767 is free\nX768 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: app(X767, .(T437, X768), T436), SCOPE: 25, CLAUSE: 3\n\nT436 is ground\nX767 is free\nX768 is free", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: app(X806, .(T466, X807), T465)\n\nT465 is ground\nX806 is free\nX807 is free", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(left(node(T242, T243, T244), X20), ','(in_order(X20, T240), ','(right(node(T242, T243, T244), X21), in_order(X21, T241)))), SCOPE: 26, CLAUSE: 4 | ','(left(node(T242, T243, T244), X20), ','(in_order(X20, T240), ','(right(node(T242, T243, T244), X21), in_order(X21, T241)))), SCOPE: 26, CLAUSE: 5\n\nT240 is ground\nT243 is ground\nT241 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(left(node(T242, T243, T244), X20), ','(in_order(X20, T240), ','(right(node(T242, T243, T244), X21), in_order(X21, T241)))), SCOPE: 26, CLAUSE: 5\n\nT240 is ground\nT243 is ground\nT241 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(in_order(T484, T240), ','(right(node(T484, T482, T485), X21), in_order(X21, T241)))\n\nT240 is ground\nT241 is ground\nT482 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: in_order(T484, T240)\n\nT240 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(right(node(T487, T482, T488), X21), in_order(X21, T241))\n\nT241 is ground\nT482 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(right(node(T487, T482, T488), X21), in_order(X21, T241)), SCOPE: 27, CLAUSE: 6 | ','(right(node(T487, T482, T488), X21), in_order(X21, T241)), SCOPE: 27, CLAUSE: 7\n\nT241 is ground\nT482 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(right(node(T487, T482, T488), X21), in_order(X21, T241)), SCOPE: 27, CLAUSE: 7\n\nT241 is ground\nT482 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: in_order(T502, T241)\n\nT241 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 195 [arrowhead = none ];
195 -> 2;

196 [label="EVAL with clause\nin_order(void, X9) :- ','(!_1, eq(X9, [])).\nand substitutionT1 -> void,\nT2 -> T4,\nX9 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 196 [arrowhead = none ];
196 -> 3;

197 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 197 [arrowhead = none ];
197 -> 4;

198 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 198 [arrowhead = none ];
198 -> 5;

199 [label="ONLY EVAL with clause\nin_order(X15, X16) :- ','(value(X15, X17), ','(app(X18, .(X17, X19), X16), ','(left(X15, X20), ','(in_order(X20, X18), ','(right(X15, X21), in_order(X21, X19)))))).\nand substitutionT1 -> T12,\nX15 -> T12,\nT2 -> T11,\nX16 -> T11,\nT10 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 199 [arrowhead = none ];
199 -> 10;

200 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 200 [arrowhead = none ];
200 -> 6;

201 [label="EVAL with clause\neq(X12, X12).\nand substitutionT4 -> [],\nX12 -> [],\nT7 -> []", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 201 [arrowhead = none ];
201 -> 7;

202 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 202 [arrowhead = none ];
202 -> 8;

203 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 203 [arrowhead = none ];
203 -> 9;

204 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
10 -> 204 [arrowhead = none ];
204 -> 11;

205 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 205 [arrowhead = none ];
205 -> 12;

206 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 206 [arrowhead = none ];
206 -> 13;

207 [label="EVAL with clause\nvalue(void, X30).\nand substitutionT12 -> void,\nX17 -> X31,\nX30 -> X31", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 207 [arrowhead = none ];
207 -> 14;

208 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 208 [arrowhead = none ];
208 -> 15;

209 [label="EVAL with clause\nvalue(node(X482, X483, X484), X483).\nand substitutionX482 -> T234,\nX483 -> T233,\nX484 -> T235,\nT12 -> node(T234, T233, T235),\nX17 -> T233,\nT231 -> T233,\nT230 -> T234,\nT232 -> T235", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 209 [arrowhead = none ];
209 -> 110;

210 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 210 [arrowhead = none ];
210 -> 111;

211 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
14 -> 211 [arrowhead = none ];
211 -> 16;

212 [label="SPLIT 2\nnew knowledge:\nT17 is ground\nT18 is ground\nT19 is ground\nT11 is ground\nreplacements:X18 -> T17,\nX31 -> T18,\nX19 -> T19", fontsize=14, style = filled, fillcolor = violet];
14 -> 212 [arrowhead = none ];
212 -> 17;

213 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 213 [arrowhead = none ];
213 -> 18;

214 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 214 [arrowhead = none ];
214 -> 91;

215 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 215 [arrowhead = none ];
215 -> 19;

216 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 216 [arrowhead = none ];
216 -> 20;

217 [label="EVAL with clause\napp([], X56, X56).\nand substitutionX18 -> [],\nX31 -> T32,\nX19 -> T33,\nX56 -> .(T32, T33),\nX57 -> T32,\nX58 -> T33,\nT11 -> .(T32, T33)", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 217 [arrowhead = none ];
217 -> 21;

218 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 218 [arrowhead = none ];
218 -> 22;

219 [label="EVAL with clause\napp(.(X75, X76), X77, .(X75, X78)) :- app(X76, X77, X78).\nand substitutionX75 -> T38,\nX76 -> X80,\nX18 -> .(T38, X80),\nX31 -> X81,\nX19 -> X82,\nX77 -> .(X81, X82),\nX79 -> T38,\nX78 -> T39,\nT11 -> .(T38, T39)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 219 [arrowhead = none ];
219 -> 24;

220 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 220 [arrowhead = none ];
220 -> 25;

221 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 221 [arrowhead = none ];
221 -> 23;

222 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
24 -> 222 [arrowhead = none ];
222 -> 26;

223 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 223 [arrowhead = none ];
223 -> 27;

224 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 224 [arrowhead = none ];
224 -> 28;

225 [label="EVAL with clause\napp([], X101, X101).\nand substitutionX80 -> [],\nX81 -> T52,\nX82 -> T53,\nX101 -> .(T52, T53),\nX102 -> T52,\nX103 -> T53,\nT39 -> .(T52, T53)", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 225 [arrowhead = none ];
225 -> 29;

226 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 226 [arrowhead = none ];
226 -> 30;

227 [label="EVAL with clause\napp(.(X120, X121), X122, .(X120, X123)) :- app(X121, X122, X123).\nand substitutionX120 -> T58,\nX121 -> X125,\nX80 -> .(T58, X125),\nX81 -> X126,\nX82 -> X127,\nX122 -> .(X126, X127),\nX124 -> T58,\nX123 -> T59,\nT39 -> .(T58, T59)", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 227 [arrowhead = none ];
227 -> 32;

228 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 228 [arrowhead = none ];
228 -> 33;

229 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 229 [arrowhead = none ];
229 -> 31;

230 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
32 -> 230 [arrowhead = none ];
230 -> 34;

231 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 231 [arrowhead = none ];
231 -> 35;

232 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 232 [arrowhead = none ];
232 -> 36;

233 [label="EVAL with clause\napp([], X146, X146).\nand substitutionX125 -> [],\nX126 -> T72,\nX127 -> T73,\nX146 -> .(T72, T73),\nX147 -> T72,\nX148 -> T73,\nT59 -> .(T72, T73)", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 233 [arrowhead = none ];
233 -> 37;

234 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 234 [arrowhead = none ];
234 -> 38;

235 [label="EVAL with clause\napp(.(X165, X166), X167, .(X165, X168)) :- app(X166, X167, X168).\nand substitutionX165 -> T78,\nX166 -> X170,\nX125 -> .(T78, X170),\nX126 -> X171,\nX127 -> X172,\nX167 -> .(X171, X172),\nX169 -> T78,\nX168 -> T79,\nT59 -> .(T78, T79)", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 235 [arrowhead = none ];
235 -> 40;

236 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 236 [arrowhead = none ];
236 -> 41;

237 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 237 [arrowhead = none ];
237 -> 39;

238 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
40 -> 238 [arrowhead = none ];
238 -> 42;

239 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 239 [arrowhead = none ];
239 -> 43;

240 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 240 [arrowhead = none ];
240 -> 44;

241 [label="EVAL with clause\napp([], X191, X191).\nand substitutionX170 -> [],\nX171 -> T92,\nX172 -> T93,\nX191 -> .(T92, T93),\nX192 -> T92,\nX193 -> T93,\nT79 -> .(T92, T93)", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 241 [arrowhead = none ];
241 -> 45;

242 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 242 [arrowhead = none ];
242 -> 46;

243 [label="EVAL with clause\napp(.(X210, X211), X212, .(X210, X213)) :- app(X211, X212, X213).\nand substitutionX210 -> T98,\nX211 -> X215,\nX170 -> .(T98, X215),\nX171 -> X216,\nX172 -> X217,\nX212 -> .(X216, X217),\nX214 -> T98,\nX213 -> T99,\nT79 -> .(T98, T99)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 243 [arrowhead = none ];
243 -> 48;

244 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 244 [arrowhead = none ];
244 -> 49;

245 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 245 [arrowhead = none ];
245 -> 47;

246 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
48 -> 246 [arrowhead = none ];
246 -> 50;

247 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 247 [arrowhead = none ];
247 -> 51;

248 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 248 [arrowhead = none ];
248 -> 52;

249 [label="EVAL with clause\napp([], X236, X236).\nand substitutionX215 -> [],\nX216 -> T112,\nX217 -> T113,\nX236 -> .(T112, T113),\nX237 -> T112,\nX238 -> T113,\nT99 -> .(T112, T113)", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 249 [arrowhead = none ];
249 -> 53;

250 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 250 [arrowhead = none ];
250 -> 54;

251 [label="EVAL with clause\napp(.(X255, X256), X257, .(X255, X258)) :- app(X256, X257, X258).\nand substitutionX255 -> T118,\nX256 -> X260,\nX215 -> .(T118, X260),\nX216 -> X261,\nX217 -> X262,\nX257 -> .(X261, X262),\nX259 -> T118,\nX258 -> T119,\nT99 -> .(T118, T119)", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 251 [arrowhead = none ];
251 -> 56;

252 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 252 [arrowhead = none ];
252 -> 57;

253 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 253 [arrowhead = none ];
253 -> 55;

254 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
56 -> 254 [arrowhead = none ];
254 -> 58;

255 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 255 [arrowhead = none ];
255 -> 59;

256 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 256 [arrowhead = none ];
256 -> 60;

257 [label="EVAL with clause\napp([], X281, X281).\nand substitutionX260 -> [],\nX261 -> T132,\nX262 -> T133,\nX281 -> .(T132, T133),\nX282 -> T132,\nX283 -> T133,\nT119 -> .(T132, T133)", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 257 [arrowhead = none ];
257 -> 61;

258 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 258 [arrowhead = none ];
258 -> 62;

259 [label="EVAL with clause\napp(.(X300, X301), X302, .(X300, X303)) :- app(X301, X302, X303).\nand substitutionX300 -> T138,\nX301 -> X305,\nX260 -> .(T138, X305),\nX261 -> X306,\nX262 -> X307,\nX302 -> .(X306, X307),\nX304 -> T138,\nX303 -> T139,\nT119 -> .(T138, T139)", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 259 [arrowhead = none ];
259 -> 64;

260 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 260 [arrowhead = none ];
260 -> 65;

261 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 261 [arrowhead = none ];
261 -> 63;

262 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
64 -> 262 [arrowhead = none ];
262 -> 66;

263 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 263 [arrowhead = none ];
263 -> 67;

264 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 264 [arrowhead = none ];
264 -> 68;

265 [label="EVAL with clause\napp([], X326, X326).\nand substitutionX305 -> [],\nX306 -> T152,\nX307 -> T153,\nX326 -> .(T152, T153),\nX327 -> T152,\nX328 -> T153,\nT139 -> .(T152, T153)", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 265 [arrowhead = none ];
265 -> 69;

266 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 266 [arrowhead = none ];
266 -> 70;

267 [label="EVAL with clause\napp(.(X345, X346), X347, .(X345, X348)) :- app(X346, X347, X348).\nand substitutionX345 -> T158,\nX346 -> X350,\nX305 -> .(T158, X350),\nX306 -> X351,\nX307 -> X352,\nX347 -> .(X351, X352),\nX349 -> T158,\nX348 -> T159,\nT139 -> .(T158, T159)", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 267 [arrowhead = none ];
267 -> 72;

268 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 268 [arrowhead = none ];
268 -> 73;

269 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 269 [arrowhead = none ];
269 -> 71;

270 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
72 -> 270 [arrowhead = none ];
270 -> 74;

271 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 271 [arrowhead = none ];
271 -> 75;

272 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 272 [arrowhead = none ];
272 -> 76;

273 [label="EVAL with clause\napp([], X371, X371).\nand substitutionX350 -> [],\nX351 -> T172,\nX352 -> T173,\nX371 -> .(T172, T173),\nX372 -> T172,\nX373 -> T173,\nT159 -> .(T172, T173)", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 273 [arrowhead = none ];
273 -> 77;

274 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 274 [arrowhead = none ];
274 -> 78;

275 [label="EVAL with clause\napp(.(X390, X391), X392, .(X390, X393)) :- app(X391, X392, X393).\nand substitutionX390 -> T178,\nX391 -> X395,\nX350 -> .(T178, X395),\nX351 -> X396,\nX352 -> X397,\nX392 -> .(X396, X397),\nX394 -> T178,\nX393 -> T179,\nT159 -> .(T178, T179)", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 275 [arrowhead = none ];
275 -> 80;

276 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 276 [arrowhead = none ];
276 -> 81;

277 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 277 [arrowhead = none ];
277 -> 79;

278 [label="GENERALIZATION\nT184 <-- .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179)))))))\n\nNew Knowledge:\nT184 is ground", fontsize=14, style = filled, fillcolor = violet];
80 -> 278 [arrowhead = none ];
278 -> 82;

279 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
82 -> 279 [arrowhead = none ];
279 -> 83;

280 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
83 -> 280 [arrowhead = none ];
280 -> 84;

281 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
83 -> 281 [arrowhead = none ];
281 -> 85;

282 [label="EVAL with clause\napp([], X422, X422).\nand substitutionX395 -> [],\nX396 -> T197,\nX397 -> T198,\nX422 -> .(T197, T198),\nX423 -> T197,\nX424 -> T198,\nT179 -> .(T197, T198)", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 282 [arrowhead = none ];
282 -> 86;

283 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 283 [arrowhead = none ];
283 -> 87;

284 [label="EVAL with clause\napp(.(X441, X442), X443, .(X441, X444)) :- app(X442, X443, X444).\nand substitutionX441 -> T203,\nX442 -> X446,\nX395 -> .(T203, X446),\nX396 -> X447,\nX397 -> X448,\nX443 -> .(X447, X448),\nX445 -> T203,\nX444 -> T204,\nT179 -> .(T203, T204)", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 284 [arrowhead = none ];
284 -> 89;

285 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 285 [arrowhead = none ];
285 -> 90;

286 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 286 [arrowhead = none ];
286 -> 88;

287 [label="INSTANCE with matching:\nX395 -> X446\nX396 -> X447\nX397 -> X448\nT179 -> T204", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 287 [arrowhead = none , style=dashed];
287 -> 82[style=dashed];

288 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
91 -> 288 [arrowhead = none ];
288 -> 92;

289 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
91 -> 289 [arrowhead = none ];
289 -> 93;

290 [label="ONLY EVAL with clause\nleft(void, void).\nand substitutionX20 -> void", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 290 [arrowhead = none ];
290 -> 94;

291 [label="BACKTRACK\nfor clause: left(node(L, X1, X2), L)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 291 [arrowhead = none ];
291 -> 109;

292 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
94 -> 292 [arrowhead = none ];
292 -> 95;

293 [label="SPLIT 2\nnew knowledge:\nT17 is ground", fontsize=14, style = filled, fillcolor = violet];
94 -> 293 [arrowhead = none ];
293 -> 96;

294 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
95 -> 294 [arrowhead = none ];
294 -> 97;

295 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
96 -> 295 [arrowhead = none ];
295 -> 104;

296 [label="ONLY EVAL with clause\nin_order(void, X462) :- ','(!_14, eq(X462, [])).\nand substitutionT17 -> T216,\nX462 -> T216", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 296 [arrowhead = none ];
296 -> 98;

297 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 297 [arrowhead = none ];
297 -> 99;

298 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
99 -> 298 [arrowhead = none ];
298 -> 100;

299 [label="EVAL with clause\neq(X465, X465).\nand substitutionT216 -> [],\nX465 -> [],\nT219 -> []", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 299 [arrowhead = none ];
299 -> 101;

300 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 300 [arrowhead = none ];
300 -> 102;

301 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 301 [arrowhead = none ];
301 -> 103;

302 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
104 -> 302 [arrowhead = none ];
302 -> 105;

303 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
104 -> 303 [arrowhead = none ];
303 -> 106;

304 [label="ONLY EVAL with clause\nright(void, void).\nand substitutionX21 -> void", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 304 [arrowhead = none ];
304 -> 107;

305 [label="BACKTRACK\nfor clause: right(node(X3, X4, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 305 [arrowhead = none ];
305 -> 108;

306 [label="INSTANCE with matching:\nT17 -> T19", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 306 [arrowhead = none , style=dashed];
306 -> 95[style=dashed];

307 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
110 -> 307 [arrowhead = none ];
307 -> 112;

308 [label="SPLIT 2\nnew knowledge:\nT240 is ground\nT243 is ground\nT241 is ground\nT11 is ground\nreplacements:X18 -> T240,\nX19 -> T241,\nT234 -> T242,\nT233 -> T243,\nT235 -> T244,\nT1 -> T245", fontsize=14, style = filled, fillcolor = violet];
110 -> 308 [arrowhead = none ];
308 -> 113;

309 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
112 -> 309 [arrowhead = none ];
309 -> 114;

310 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
113 -> 310 [arrowhead = none ];
310 -> 187;

311 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
114 -> 311 [arrowhead = none ];
311 -> 115;

312 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
114 -> 312 [arrowhead = none ];
312 -> 116;

313 [label="EVAL with clause\napp([], X501, X501).\nand substitutionX18 -> [],\nT233 -> T258,\nX19 -> T259,\nX501 -> .(T258, T259),\nX502 -> T259,\nT11 -> .(T258, T259)", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 313 [arrowhead = none ];
313 -> 117;

314 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 314 [arrowhead = none ];
314 -> 118;

315 [label="EVAL with clause\napp(.(X517, X518), X519, .(X517, X520)) :- app(X518, X519, X520).\nand substitutionX517 -> T267,\nX518 -> X522,\nX18 -> .(T267, X522),\nT233 -> T269,\nX19 -> X523,\nX519 -> .(T269, X523),\nX521 -> T267,\nX520 -> T268,\nT11 -> .(T267, T268),\nT266 -> T269", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 315 [arrowhead = none ];
315 -> 120;

316 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 316 [arrowhead = none ];
316 -> 121;

317 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 317 [arrowhead = none ];
317 -> 119;

318 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
120 -> 318 [arrowhead = none ];
318 -> 122;

319 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
122 -> 319 [arrowhead = none ];
319 -> 123;

320 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
122 -> 320 [arrowhead = none ];
320 -> 124;

321 [label="EVAL with clause\napp([], X536, X536).\nand substitutionX522 -> [],\nT269 -> T282,\nX523 -> T283,\nX536 -> .(T282, T283),\nX537 -> T283,\nT268 -> .(T282, T283)", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 321 [arrowhead = none ];
321 -> 125;

322 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 322 [arrowhead = none ];
322 -> 126;

323 [label="EVAL with clause\napp(.(X552, X553), X554, .(X552, X555)) :- app(X553, X554, X555).\nand substitutionX552 -> T291,\nX553 -> X557,\nX522 -> .(T291, X557),\nT269 -> T293,\nX523 -> X558,\nX554 -> .(T293, X558),\nX556 -> T291,\nX555 -> T292,\nT268 -> .(T291, T292),\nT290 -> T293", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 323 [arrowhead = none ];
323 -> 128;

324 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 324 [arrowhead = none ];
324 -> 129;

325 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 325 [arrowhead = none ];
325 -> 127;

326 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
128 -> 326 [arrowhead = none ];
326 -> 130;

327 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
130 -> 327 [arrowhead = none ];
327 -> 131;

328 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
130 -> 328 [arrowhead = none ];
328 -> 132;

329 [label="EVAL with clause\napp([], X571, X571).\nand substitutionX557 -> [],\nT293 -> T306,\nX558 -> T307,\nX571 -> .(T306, T307),\nX572 -> T307,\nT292 -> .(T306, T307)", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 329 [arrowhead = none ];
329 -> 133;

330 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
131 -> 330 [arrowhead = none ];
330 -> 134;

331 [label="EVAL with clause\napp(.(X587, X588), X589, .(X587, X590)) :- app(X588, X589, X590).\nand substitutionX587 -> T315,\nX588 -> X592,\nX557 -> .(T315, X592),\nT293 -> T317,\nX558 -> X593,\nX589 -> .(T317, X593),\nX591 -> T315,\nX590 -> T316,\nT292 -> .(T315, T316),\nT314 -> T317", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 331 [arrowhead = none ];
331 -> 136;

332 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 332 [arrowhead = none ];
332 -> 137;

333 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 333 [arrowhead = none ];
333 -> 135;

334 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
136 -> 334 [arrowhead = none ];
334 -> 138;

335 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 335 [arrowhead = none ];
335 -> 139;

336 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 336 [arrowhead = none ];
336 -> 140;

337 [label="EVAL with clause\napp([], X606, X606).\nand substitutionX592 -> [],\nT317 -> T330,\nX593 -> T331,\nX606 -> .(T330, T331),\nX607 -> T331,\nT316 -> .(T330, T331)", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 337 [arrowhead = none ];
337 -> 141;

338 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 338 [arrowhead = none ];
338 -> 142;

339 [label="EVAL with clause\napp(.(X622, X623), X624, .(X622, X625)) :- app(X623, X624, X625).\nand substitutionX622 -> T339,\nX623 -> X627,\nX592 -> .(T339, X627),\nT317 -> T341,\nX593 -> X628,\nX624 -> .(T341, X628),\nX626 -> T339,\nX625 -> T340,\nT316 -> .(T339, T340),\nT338 -> T341", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 339 [arrowhead = none ];
339 -> 144;

340 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 340 [arrowhead = none ];
340 -> 145;

341 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 341 [arrowhead = none ];
341 -> 143;

342 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
144 -> 342 [arrowhead = none ];
342 -> 146;

343 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
146 -> 343 [arrowhead = none ];
343 -> 147;

344 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
146 -> 344 [arrowhead = none ];
344 -> 148;

345 [label="EVAL with clause\napp([], X641, X641).\nand substitutionX627 -> [],\nT341 -> T354,\nX628 -> T355,\nX641 -> .(T354, T355),\nX642 -> T355,\nT340 -> .(T354, T355)", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 345 [arrowhead = none ];
345 -> 149;

346 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 346 [arrowhead = none ];
346 -> 150;

347 [label="EVAL with clause\napp(.(X657, X658), X659, .(X657, X660)) :- app(X658, X659, X660).\nand substitutionX657 -> T363,\nX658 -> X662,\nX627 -> .(T363, X662),\nT341 -> T365,\nX628 -> X663,\nX659 -> .(T365, X663),\nX661 -> T363,\nX660 -> T364,\nT340 -> .(T363, T364),\nT362 -> T365", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 347 [arrowhead = none ];
347 -> 152;

348 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 348 [arrowhead = none ];
348 -> 153;

349 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 349 [arrowhead = none ];
349 -> 151;

350 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
152 -> 350 [arrowhead = none ];
350 -> 154;

351 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
154 -> 351 [arrowhead = none ];
351 -> 155;

352 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
154 -> 352 [arrowhead = none ];
352 -> 156;

353 [label="EVAL with clause\napp([], X676, X676).\nand substitutionX662 -> [],\nT365 -> T378,\nX663 -> T379,\nX676 -> .(T378, T379),\nX677 -> T379,\nT364 -> .(T378, T379)", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 353 [arrowhead = none ];
353 -> 157;

354 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 354 [arrowhead = none ];
354 -> 158;

355 [label="EVAL with clause\napp(.(X692, X693), X694, .(X692, X695)) :- app(X693, X694, X695).\nand substitutionX692 -> T387,\nX693 -> X697,\nX662 -> .(T387, X697),\nT365 -> T389,\nX663 -> X698,\nX694 -> .(T389, X698),\nX696 -> T387,\nX695 -> T388,\nT364 -> .(T387, T388),\nT386 -> T389", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 355 [arrowhead = none ];
355 -> 160;

356 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
156 -> 356 [arrowhead = none ];
356 -> 161;

357 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 357 [arrowhead = none ];
357 -> 159;

358 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
160 -> 358 [arrowhead = none ];
358 -> 162;

359 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
162 -> 359 [arrowhead = none ];
359 -> 163;

360 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
162 -> 360 [arrowhead = none ];
360 -> 164;

361 [label="EVAL with clause\napp([], X711, X711).\nand substitutionX697 -> [],\nT389 -> T402,\nX698 -> T403,\nX711 -> .(T402, T403),\nX712 -> T403,\nT388 -> .(T402, T403)", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 361 [arrowhead = none ];
361 -> 165;

362 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
163 -> 362 [arrowhead = none ];
362 -> 166;

363 [label="EVAL with clause\napp(.(X727, X728), X729, .(X727, X730)) :- app(X728, X729, X730).\nand substitutionX727 -> T411,\nX728 -> X732,\nX697 -> .(T411, X732),\nT389 -> T413,\nX698 -> X733,\nX729 -> .(T413, X733),\nX731 -> T411,\nX730 -> T412,\nT388 -> .(T411, T412),\nT410 -> T413", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 363 [arrowhead = none ];
363 -> 168;

364 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
164 -> 364 [arrowhead = none ];
364 -> 169;

365 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
165 -> 365 [arrowhead = none ];
365 -> 167;

366 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
168 -> 366 [arrowhead = none ];
366 -> 170;

367 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
170 -> 367 [arrowhead = none ];
367 -> 171;

368 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
170 -> 368 [arrowhead = none ];
368 -> 172;

369 [label="EVAL with clause\napp([], X746, X746).\nand substitutionX732 -> [],\nT413 -> T426,\nX733 -> T427,\nX746 -> .(T426, T427),\nX747 -> T427,\nT412 -> .(T426, T427)", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 369 [arrowhead = none ];
369 -> 173;

370 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
171 -> 370 [arrowhead = none ];
370 -> 174;

371 [label="EVAL with clause\napp(.(X762, X763), X764, .(X762, X765)) :- app(X763, X764, X765).\nand substitutionX762 -> T435,\nX763 -> X767,\nX732 -> .(T435, X767),\nT413 -> T437,\nX733 -> X768,\nX764 -> .(T437, X768),\nX766 -> T435,\nX765 -> T436,\nT412 -> .(T435, T436),\nT434 -> T437", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 371 [arrowhead = none ];
371 -> 176;

372 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 372 [arrowhead = none ];
372 -> 177;

373 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 373 [arrowhead = none ];
373 -> 175;

374 [label="GENERALIZATION\nT442 <-- .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436)))))))\n\nNew Knowledge:\nT442 is ground", fontsize=14, style = filled, fillcolor = violet];
176 -> 374 [arrowhead = none ];
374 -> 178;

375 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
178 -> 375 [arrowhead = none ];
375 -> 179;

376 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 376 [arrowhead = none ];
376 -> 180;

377 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 377 [arrowhead = none ];
377 -> 181;

378 [label="EVAL with clause\napp([], X785, X785).\nand substitutionX767 -> [],\nT437 -> T455,\nX768 -> T456,\nX785 -> .(T455, T456),\nX786 -> T456,\nT436 -> .(T455, T456)", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 378 [arrowhead = none ];
378 -> 182;

379 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
180 -> 379 [arrowhead = none ];
379 -> 183;

380 [label="EVAL with clause\napp(.(X801, X802), X803, .(X801, X804)) :- app(X802, X803, X804).\nand substitutionX801 -> T464,\nX802 -> X806,\nX767 -> .(T464, X806),\nT437 -> T466,\nX768 -> X807,\nX803 -> .(T466, X807),\nX805 -> T464,\nX804 -> T465,\nT436 -> .(T464, T465),\nT463 -> T466", fontsize=14, style = filled, fillcolor = lightblue];
181 -> 380 [arrowhead = none ];
380 -> 185;

381 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 381 [arrowhead = none ];
381 -> 186;

382 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 382 [arrowhead = none ];
382 -> 184;

383 [label="INSTANCE with matching:\nX767 -> X806\nT437 -> T466\nX768 -> X807\nT436 -> T465", fontsize=14, style = filled, fillcolor = lightgrey];
185 -> 383 [arrowhead = none , style=dashed];
383 -> 178[style=dashed];

384 [label="BACKTRACK\nfor clause: left(void, void)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
187 -> 384 [arrowhead = none ];
384 -> 188;

385 [label="ONLY EVAL with clause\nleft(node(X820, X821, X822), X820).\nand substitutionT242 -> T484,\nX820 -> T484,\nT243 -> T482,\nX821 -> T482,\nT244 -> T485,\nX822 -> T485,\nX20 -> T484,\nT481 -> T484,\nT483 -> T485", fontsize=14, style = filled, fillcolor = lightblue];
188 -> 385 [arrowhead = none ];
385 -> 189;

386 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
189 -> 386 [arrowhead = none ];
386 -> 190;

387 [label="SPLIT 2\nnew knowledge:\nT240 is ground\nreplacements:T484 -> T487,\nT485 -> T488", fontsize=14, style = filled, fillcolor = violet];
189 -> 387 [arrowhead = none ];
387 -> 191;

388 [label="INSTANCE with matching:\nT1 -> T484\nT2 -> T240", fontsize=14, style = filled, fillcolor = lightgrey];
190 -> 388 [arrowhead = none , style=dashed];
388 -> 1[style=dashed];

389 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
191 -> 389 [arrowhead = none ];
389 -> 192;

390 [label="BACKTRACK\nfor clause: right(void, void)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
192 -> 390 [arrowhead = none ];
390 -> 193;

391 [label="ONLY EVAL with clause\nright(node(X833, X834, X835), X835).\nand substitutionT487 -> T499,\nX833 -> T499,\nT482 -> T500,\nX834 -> T500,\nT488 -> T502,\nX835 -> T502,\nX21 -> T502,\nT501 -> T502", fontsize=14, style = filled, fillcolor = lightblue];
193 -> 391 [arrowhead = none ];
391 -> 194;

392 [label="INSTANCE with matching:\nT1 -> T502\nT2 -> T241", fontsize=14, style = filled, fillcolor = lightgrey];
194 -> 392 [arrowhead = none , style=dashed];
392 -> 1[style=dashed];

}

(2) Obligation:

Triples:

appA(.(X1, X2), X3, X4, .(X1, X5)) :- appA(X2, X3, X4, X5).
appC(.(X1, X2), X3, X4, .(X1, X5)) :- appC(X2, X3, X4, X5).
in_orderD(void, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) :- appA(X10, X11, X12, X9).
in_orderD(void, X1) :- ','(appcE(X2, X3, X4, X1), in_orderB(X2)).
in_orderD(void, X1) :- ','(appcE(X2, X3, X4, X1), ','(in_ordercB(X2), in_orderB(X4))).
in_orderD(node(X1, X2, X3), .(X4, .(X5, .(X6, .(X7, .(X8, .(X9, .(X10, .(X11, X12))))))))) :- appC(X13, X2, X14, X12).
in_orderD(node(X1, X2, X3), X4) :- ','(appcF(X5, X2, X6, X4), in_orderD(X1, X5)).
in_orderD(node(X1, X2, X3), X4) :- ','(appcF(X5, X2, X6, X4), ','(in_ordercD(X1, X5), in_orderD(X3, X6))).

Clauses:

appcA([], X1, X2, .(X1, X2)).
appcA(.(X1, X2), X3, X4, .(X1, X5)) :- appcA(X2, X3, X4, X5).
in_ordercB([]).
appcC([], X1, X2, .(X1, X2)).
appcC(.(X1, X2), X3, X4, .(X1, X5)) :- appcC(X2, X3, X4, X5).
in_ordercD(void, []).
in_ordercD(void, X1) :- ','(appcE(X2, X3, X4, X1), ','(in_ordercB(X2), in_ordercB(X4))).
in_ordercD(node(X1, X2, X3), X4) :- ','(appcF(X5, X2, X6, X4), ','(in_ordercD(X1, X5), in_ordercD(X3, X6))).
appcE([], X1, X2, .(X1, X2)).
appcE(.(X1, []), X2, X3, .(X1, .(X2, X3))).
appcE(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))).
appcE(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))).
appcE(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))).
appcE(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))).
appcE(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))).
appcE(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))).
appcE(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) :- appcA(X9, X10, X11, X12).
appcF([], X1, X2, .(X1, X2)).
appcF(.(X1, []), X2, X3, .(X1, .(X2, X3))).
appcF(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))).
appcF(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))).
appcF(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))).
appcF(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))).
appcF(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))).
appcF(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))).
appcF(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) :- appcC(X9, X10, X11, X12).

Afs:

in_orderD(x1, x2) = in_orderD(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

appA(.(X1, X2), X3, X4, .(X1, X5)) :- appA(X2, X3, X4, X5).
appC(.(X1, X2), X3, X4, .(X1, X5)) :- appC(X2, X3, X4, X5).
in_orderD(void, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) :- appA(X10, X11, X12, X9).
in_orderD(node(X1, X2, X3), .(X4, .(X5, .(X6, .(X7, .(X8, .(X9, .(X10, .(X11, X12))))))))) :- appC(X13, X2, X14, X12).
in_orderD(node(X1, X2, X3), X4) :- ','(appcF(X5, X2, X6, X4), in_orderD(X1, X5)).
in_orderD(node(X1, X2, X3), X4) :- ','(appcF(X5, X2, X6, X4), ','(in_ordercD(X1, X5), in_orderD(X3, X6))).

Clauses:

appcA([], X1, X2, .(X1, X2)).
appcA(.(X1, X2), X3, X4, .(X1, X5)) :- appcA(X2, X3, X4, X5).
in_ordercB([]).
appcC([], X1, X2, .(X1, X2)).
appcC(.(X1, X2), X3, X4, .(X1, X5)) :- appcC(X2, X3, X4, X5).
in_ordercD(void, []).
in_ordercD(void, X1) :- ','(appcE(X2, X3, X4, X1), ','(in_ordercB(X2), in_ordercB(X4))).
in_ordercD(node(X1, X2, X3), X4) :- ','(appcF(X5, X2, X6, X4), ','(in_ordercD(X1, X5), in_ordercD(X3, X6))).
appcE([], X1, X2, .(X1, X2)).
appcE(.(X1, []), X2, X3, .(X1, .(X2, X3))).
appcE(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))).
appcE(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))).
appcE(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))).
appcE(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))).
appcE(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))).
appcE(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))).
appcE(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) :- appcA(X9, X10, X11, X12).
appcF([], X1, X2, .(X1, X2)).
appcF(.(X1, []), X2, X3, .(X1, .(X2, X3))).
appcF(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))).
appcF(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))).
appcF(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))).
appcF(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))).
appcF(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))).
appcF(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))).
appcF(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) :- appcC(X9, X10, X11, X12).

Afs:

in_orderD(x1, x2) = in_orderD(x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
in_orderD_in: (f,b)
appA_in: (f,f,f,b)
appC_in: (f,f,f,b)
appcF_in: (f,f,f,b)
appcC_in: (f,f,f,b)
in_ordercD_in: (f,b)
appcE_in: (f,f,f,b)
appcA_in: (f,f,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

IN_ORDERD_IN_AG(void, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → U3_AG(X1, X2, X3, X4, X5, X6, X7, X8, X9, appA_in_aaag(X10, X11, X12, X9))
IN_ORDERD_IN_AG(void, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → APPA_IN_AAAG(X10, X11, X12, X9)
APPA_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → U1_AAAG(X1, X2, X3, X4, X5, appA_in_aaag(X2, X3, X4, X5))
APPA_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPA_IN_AAAG(X2, X3, X4, X5)
IN_ORDERD_IN_AG(node(X1, X2, X3), .(X4, .(X5, .(X6, .(X7, .(X8, .(X9, .(X10, .(X11, X12))))))))) → U4_AG(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appC_in_aaag(X13, X2, X14, X12))
IN_ORDERD_IN_AG(node(X1, X2, X3), .(X4, .(X5, .(X6, .(X7, .(X8, .(X9, .(X10, .(X11, X12))))))))) → APPC_IN_AAAG(X13, X2, X14, X12)
APPC_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → U2_AAAG(X1, X2, X3, X4, X5, appC_in_aaag(X2, X3, X4, X5))
APPC_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPC_IN_AAAG(X2, X3, X4, X5)
IN_ORDERD_IN_AG(node(X1, X2, X3), X4) → U5_AG(X1, X2, X3, X4, appcF_in_aaag(X5, X2, X6, X4))
U5_AG(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U6_AG(X1, X2, X3, X4, in_orderD_in_ag(X1, X5))
U5_AG(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X1, X5)
U5_AG(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U7_AG(X1, X2, X3, X4, X6, in_ordercD_in_ag(X1, X5))
U7_AG(X1, X2, X3, X4, X6, in_ordercD_out_ag(X1, X5)) → U8_AG(X1, X2, X3, X4, in_orderD_in_ag(X3, X6))
U7_AG(X1, X2, X3, X4, X6, in_ordercD_out_ag(X1, X5)) → IN_ORDERD_IN_AG(X3, X6)

The TRS R consists of the following rules:

appcF_in_aaag([], X1, X2, .(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_in_aaag(X9, X10, X11, X12))
appcC_in_aaag([], X1, X2, .(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, appcC_in_aaag(X2, X3, X4, X5))
U11_aaag(X1, X2, X3, X4, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
in_ordercD_in_ag(void, []) → in_ordercD_out_ag(void, [])
in_ordercD_in_ag(void, X1) → U12_ag(X1, appcE_in_aaag(X2, X3, X4, X1))
appcE_in_aaag([], X1, X2, .(X1, X2)) → appcE_out_aaag([], X1, X2, .(X1, X2))
appcE_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcE_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcE_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcE_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcE_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcE_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_in_aaag(X9, X10, X11, X12))
appcA_in_aaag([], X1, X2, .(X1, X2)) → appcA_out_aaag([], X1, X2, .(X1, X2))
appcA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U10_aaag(X1, X2, X3, X4, X5, appcA_in_aaag(X2, X3, X4, X5))
U10_aaag(X1, X2, X3, X4, X5, appcA_out_aaag(X2, X3, X4, X5)) → appcA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_out_aaag(X9, X10, X11, X12)) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U12_ag(X1, appcE_out_aaag(X2, X3, X4, X1)) → U13_ag(X1, X2, X3, X4, in_ordercB_in_g(X2))
in_ordercB_in_g([]) → in_ordercB_out_g([])
U13_ag(X1, X2, X3, X4, in_ordercB_out_g(X2)) → U14_ag(X1, in_ordercB_in_g(X4))
U14_ag(X1, in_ordercB_out_g(X4)) → in_ordercD_out_ag(void, X1)
in_ordercD_in_ag(node(X1, X2, X3), X4) → U15_ag(X1, X2, X3, X4, appcF_in_aaag(X5, X2, X6, X4))
U15_ag(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_in_ag(X1, X5))
U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_out_ag(X1, X5)) → U17_ag(X1, X2, X3, X4, in_ordercD_in_ag(X3, X6))
U17_ag(X1, X2, X3, X4, in_ordercD_out_ag(X3, X6)) → in_ordercD_out_ag(node(X1, X2, X3), X4)

The argument filtering Pi contains the following mapping:
in_orderD_in_ag(x1, x2) = in_orderD_in_ag(x2)
.(x1, x2) = .(x1, x2)
appA_in_aaag(x1, x2, x3, x4) = appA_in_aaag(x4)
appC_in_aaag(x1, x2, x3, x4) = appC_in_aaag(x4)
appcF_in_aaag(x1, x2, x3, x4) = appcF_in_aaag(x4)
appcF_out_aaag(x1, x2, x3, x4) = appcF_out_aaag(x1, x2, x3, x4)
U19_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U19_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x12, x13)
appcC_in_aaag(x1, x2, x3, x4) = appcC_in_aaag(x4)
appcC_out_aaag(x1, x2, x3, x4) = appcC_out_aaag(x1, x2, x3, x4)
U11_aaag(x1, x2, x3, x4, x5, x6) = U11_aaag(x1, x5, x6)
in_ordercD_in_ag(x1, x2) = in_ordercD_in_ag(x2)
[] = []
in_ordercD_out_ag(x1, x2) = in_ordercD_out_ag(x1, x2)
U12_ag(x1, x2) = U12_ag(x1, x2)
appcE_in_aaag(x1, x2, x3, x4) = appcE_in_aaag(x4)
appcE_out_aaag(x1, x2, x3, x4) = appcE_out_aaag(x1, x2, x3, x4)
U18_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U18_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x12, x13)
appcA_in_aaag(x1, x2, x3, x4) = appcA_in_aaag(x4)
appcA_out_aaag(x1, x2, x3, x4) = appcA_out_aaag(x1, x2, x3, x4)
U10_aaag(x1, x2, x3, x4, x5, x6) = U10_aaag(x1, x5, x6)
U13_ag(x1, x2, x3, x4, x5) = U13_ag(x1, x4, x5)
in_ordercB_in_g(x1) = in_ordercB_in_g(x1)
in_ordercB_out_g(x1) = in_ordercB_out_g(x1)
U14_ag(x1, x2) = U14_ag(x1, x2)
U15_ag(x1, x2, x3, x4, x5) = U15_ag(x4, x5)
U16_ag(x1, x2, x3, x4, x5, x6, x7) = U16_ag(x2, x4, x6, x7)
U17_ag(x1, x2, x3, x4, x5) = U17_ag(x1, x2, x4, x5)
void = void
node(x1, x2, x3) = node(x1, x2, x3)
IN_ORDERD_IN_AG(x1, x2) = IN_ORDERD_IN_AG(x2)
U3_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U3_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
APPA_IN_AAAG(x1, x2, x3, x4) = APPA_IN_AAAG(x4)
U1_AAAG(x1, x2, x3, x4, x5, x6) = U1_AAAG(x1, x5, x6)
U4_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U4_AG(x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
APPC_IN_AAAG(x1, x2, x3, x4) = APPC_IN_AAAG(x4)
U2_AAAG(x1, x2, x3, x4, x5, x6) = U2_AAAG(x1, x5, x6)
U5_AG(x1, x2, x3, x4, x5) = U5_AG(x4, x5)
U6_AG(x1, x2, x3, x4, x5) = U6_AG(x4, x5)
U7_AG(x1, x2, x3, x4, x5, x6) = U7_AG(x4, x5, x6)
U8_AG(x1, x2, x3, x4, x5) = U8_AG(x4, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

IN_ORDERD_IN_AG(void, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → U3_AG(X1, X2, X3, X4, X5, X6, X7, X8, X9, appA_in_aaag(X10, X11, X12, X9))
IN_ORDERD_IN_AG(void, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → APPA_IN_AAAG(X10, X11, X12, X9)
APPA_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → U1_AAAG(X1, X2, X3, X4, X5, appA_in_aaag(X2, X3, X4, X5))
APPA_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPA_IN_AAAG(X2, X3, X4, X5)
IN_ORDERD_IN_AG(node(X1, X2, X3), .(X4, .(X5, .(X6, .(X7, .(X8, .(X9, .(X10, .(X11, X12))))))))) → U4_AG(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appC_in_aaag(X13, X2, X14, X12))
IN_ORDERD_IN_AG(node(X1, X2, X3), .(X4, .(X5, .(X6, .(X7, .(X8, .(X9, .(X10, .(X11, X12))))))))) → APPC_IN_AAAG(X13, X2, X14, X12)
APPC_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → U2_AAAG(X1, X2, X3, X4, X5, appC_in_aaag(X2, X3, X4, X5))
APPC_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPC_IN_AAAG(X2, X3, X4, X5)
IN_ORDERD_IN_AG(node(X1, X2, X3), X4) → U5_AG(X1, X2, X3, X4, appcF_in_aaag(X5, X2, X6, X4))
U5_AG(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U6_AG(X1, X2, X3, X4, in_orderD_in_ag(X1, X5))
U5_AG(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X1, X5)
U5_AG(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U7_AG(X1, X2, X3, X4, X6, in_ordercD_in_ag(X1, X5))
U7_AG(X1, X2, X3, X4, X6, in_ordercD_out_ag(X1, X5)) → U8_AG(X1, X2, X3, X4, in_orderD_in_ag(X3, X6))
U7_AG(X1, X2, X3, X4, X6, in_ordercD_out_ag(X1, X5)) → IN_ORDERD_IN_AG(X3, X6)

The TRS R consists of the following rules:

appcF_in_aaag([], X1, X2, .(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_in_aaag(X9, X10, X11, X12))
appcC_in_aaag([], X1, X2, .(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, appcC_in_aaag(X2, X3, X4, X5))
U11_aaag(X1, X2, X3, X4, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
in_ordercD_in_ag(void, []) → in_ordercD_out_ag(void, [])
in_ordercD_in_ag(void, X1) → U12_ag(X1, appcE_in_aaag(X2, X3, X4, X1))
appcE_in_aaag([], X1, X2, .(X1, X2)) → appcE_out_aaag([], X1, X2, .(X1, X2))
appcE_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcE_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcE_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcE_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcE_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcE_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_in_aaag(X9, X10, X11, X12))
appcA_in_aaag([], X1, X2, .(X1, X2)) → appcA_out_aaag([], X1, X2, .(X1, X2))
appcA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U10_aaag(X1, X2, X3, X4, X5, appcA_in_aaag(X2, X3, X4, X5))
U10_aaag(X1, X2, X3, X4, X5, appcA_out_aaag(X2, X3, X4, X5)) → appcA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_out_aaag(X9, X10, X11, X12)) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U12_ag(X1, appcE_out_aaag(X2, X3, X4, X1)) → U13_ag(X1, X2, X3, X4, in_ordercB_in_g(X2))
in_ordercB_in_g([]) → in_ordercB_out_g([])
U13_ag(X1, X2, X3, X4, in_ordercB_out_g(X2)) → U14_ag(X1, in_ordercB_in_g(X4))
U14_ag(X1, in_ordercB_out_g(X4)) → in_ordercD_out_ag(void, X1)
in_ordercD_in_ag(node(X1, X2, X3), X4) → U15_ag(X1, X2, X3, X4, appcF_in_aaag(X5, X2, X6, X4))
U15_ag(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_in_ag(X1, X5))
U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_out_ag(X1, X5)) → U17_ag(X1, X2, X3, X4, in_ordercD_in_ag(X3, X6))
U17_ag(X1, X2, X3, X4, in_ordercD_out_ag(X3, X6)) → in_ordercD_out_ag(node(X1, X2, X3), X4)

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 8 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPC_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPC_IN_AAAG(X2, X3, X4, X5)

The TRS R consists of the following rules:

appcF_in_aaag([], X1, X2, .(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_in_aaag(X9, X10, X11, X12))
appcC_in_aaag([], X1, X2, .(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, appcC_in_aaag(X2, X3, X4, X5))
U11_aaag(X1, X2, X3, X4, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
in_ordercD_in_ag(void, []) → in_ordercD_out_ag(void, [])
in_ordercD_in_ag(void, X1) → U12_ag(X1, appcE_in_aaag(X2, X3, X4, X1))
appcE_in_aaag([], X1, X2, .(X1, X2)) → appcE_out_aaag([], X1, X2, .(X1, X2))
appcE_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcE_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcE_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcE_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcE_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcE_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_in_aaag(X9, X10, X11, X12))
appcA_in_aaag([], X1, X2, .(X1, X2)) → appcA_out_aaag([], X1, X2, .(X1, X2))
appcA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U10_aaag(X1, X2, X3, X4, X5, appcA_in_aaag(X2, X3, X4, X5))
U10_aaag(X1, X2, X3, X4, X5, appcA_out_aaag(X2, X3, X4, X5)) → appcA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_out_aaag(X9, X10, X11, X12)) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U12_ag(X1, appcE_out_aaag(X2, X3, X4, X1)) → U13_ag(X1, X2, X3, X4, in_ordercB_in_g(X2))
in_ordercB_in_g([]) → in_ordercB_out_g([])
U13_ag(X1, X2, X3, X4, in_ordercB_out_g(X2)) → U14_ag(X1, in_ordercB_in_g(X4))
U14_ag(X1, in_ordercB_out_g(X4)) → in_ordercD_out_ag(void, X1)
in_ordercD_in_ag(node(X1, X2, X3), X4) → U15_ag(X1, X2, X3, X4, appcF_in_aaag(X5, X2, X6, X4))
U15_ag(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_in_ag(X1, X5))
U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_out_ag(X1, X5)) → U17_ag(X1, X2, X3, X4, in_ordercD_in_ag(X3, X6))
U17_ag(X1, X2, X3, X4, in_ordercD_out_ag(X3, X6)) → in_ordercD_out_ag(node(X1, X2, X3), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
appcF_in_aaag(x1, x2, x3, x4) = appcF_in_aaag(x4)
appcF_out_aaag(x1, x2, x3, x4) = appcF_out_aaag(x1, x2, x3, x4)
U19_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U19_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x12, x13)
appcC_in_aaag(x1, x2, x3, x4) = appcC_in_aaag(x4)
appcC_out_aaag(x1, x2, x3, x4) = appcC_out_aaag(x1, x2, x3, x4)
U11_aaag(x1, x2, x3, x4, x5, x6) = U11_aaag(x1, x5, x6)
in_ordercD_in_ag(x1, x2) = in_ordercD_in_ag(x2)
[] = []
in_ordercD_out_ag(x1, x2) = in_ordercD_out_ag(x1, x2)
U12_ag(x1, x2) = U12_ag(x1, x2)
appcE_in_aaag(x1, x2, x3, x4) = appcE_in_aaag(x4)
appcE_out_aaag(x1, x2, x3, x4) = appcE_out_aaag(x1, x2, x3, x4)
U18_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U18_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x12, x13)
appcA_in_aaag(x1, x2, x3, x4) = appcA_in_aaag(x4)
appcA_out_aaag(x1, x2, x3, x4) = appcA_out_aaag(x1, x2, x3, x4)
U10_aaag(x1, x2, x3, x4, x5, x6) = U10_aaag(x1, x5, x6)
U13_ag(x1, x2, x3, x4, x5) = U13_ag(x1, x4, x5)
in_ordercB_in_g(x1) = in_ordercB_in_g(x1)
in_ordercB_out_g(x1) = in_ordercB_out_g(x1)
U14_ag(x1, x2) = U14_ag(x1, x2)
U15_ag(x1, x2, x3, x4, x5) = U15_ag(x4, x5)
U16_ag(x1, x2, x3, x4, x5, x6, x7) = U16_ag(x2, x4, x6, x7)
U17_ag(x1, x2, x3, x4, x5) = U17_ag(x1, x2, x4, x5)
void = void
node(x1, x2, x3) = node(x1, x2, x3)
APPC_IN_AAAG(x1, x2, x3, x4) = APPC_IN_AAAG(x4)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPC_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPC_IN_AAAG(X2, X3, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
APPC_IN_AAAG(x1, x2, x3, x4) = APPC_IN_AAAG(x4)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPC_IN_AAAG(.(X1, X5)) → APPC_IN_AAAG(X5)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APPC_IN_AAAG(.(X1, X5)) → APPC_IN_AAAG(X5)
The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPA_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPA_IN_AAAG(X2, X3, X4, X5)

The TRS R consists of the following rules:

appcF_in_aaag([], X1, X2, .(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_in_aaag(X9, X10, X11, X12))
appcC_in_aaag([], X1, X2, .(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, appcC_in_aaag(X2, X3, X4, X5))
U11_aaag(X1, X2, X3, X4, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
in_ordercD_in_ag(void, []) → in_ordercD_out_ag(void, [])
in_ordercD_in_ag(void, X1) → U12_ag(X1, appcE_in_aaag(X2, X3, X4, X1))
appcE_in_aaag([], X1, X2, .(X1, X2)) → appcE_out_aaag([], X1, X2, .(X1, X2))
appcE_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcE_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcE_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcE_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcE_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcE_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_in_aaag(X9, X10, X11, X12))
appcA_in_aaag([], X1, X2, .(X1, X2)) → appcA_out_aaag([], X1, X2, .(X1, X2))
appcA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U10_aaag(X1, X2, X3, X4, X5, appcA_in_aaag(X2, X3, X4, X5))
U10_aaag(X1, X2, X3, X4, X5, appcA_out_aaag(X2, X3, X4, X5)) → appcA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_out_aaag(X9, X10, X11, X12)) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U12_ag(X1, appcE_out_aaag(X2, X3, X4, X1)) → U13_ag(X1, X2, X3, X4, in_ordercB_in_g(X2))
in_ordercB_in_g([]) → in_ordercB_out_g([])
U13_ag(X1, X2, X3, X4, in_ordercB_out_g(X2)) → U14_ag(X1, in_ordercB_in_g(X4))
U14_ag(X1, in_ordercB_out_g(X4)) → in_ordercD_out_ag(void, X1)
in_ordercD_in_ag(node(X1, X2, X3), X4) → U15_ag(X1, X2, X3, X4, appcF_in_aaag(X5, X2, X6, X4))
U15_ag(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_in_ag(X1, X5))
U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_out_ag(X1, X5)) → U17_ag(X1, X2, X3, X4, in_ordercD_in_ag(X3, X6))
U17_ag(X1, X2, X3, X4, in_ordercD_out_ag(X3, X6)) → in_ordercD_out_ag(node(X1, X2, X3), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
appcF_in_aaag(x1, x2, x3, x4) = appcF_in_aaag(x4)
appcF_out_aaag(x1, x2, x3, x4) = appcF_out_aaag(x1, x2, x3, x4)
U19_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U19_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x12, x13)
appcC_in_aaag(x1, x2, x3, x4) = appcC_in_aaag(x4)
appcC_out_aaag(x1, x2, x3, x4) = appcC_out_aaag(x1, x2, x3, x4)
U11_aaag(x1, x2, x3, x4, x5, x6) = U11_aaag(x1, x5, x6)
in_ordercD_in_ag(x1, x2) = in_ordercD_in_ag(x2)
[] = []
in_ordercD_out_ag(x1, x2) = in_ordercD_out_ag(x1, x2)
U12_ag(x1, x2) = U12_ag(x1, x2)
appcE_in_aaag(x1, x2, x3, x4) = appcE_in_aaag(x4)
appcE_out_aaag(x1, x2, x3, x4) = appcE_out_aaag(x1, x2, x3, x4)
U18_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U18_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x12, x13)
appcA_in_aaag(x1, x2, x3, x4) = appcA_in_aaag(x4)
appcA_out_aaag(x1, x2, x3, x4) = appcA_out_aaag(x1, x2, x3, x4)
U10_aaag(x1, x2, x3, x4, x5, x6) = U10_aaag(x1, x5, x6)
U13_ag(x1, x2, x3, x4, x5) = U13_ag(x1, x4, x5)
in_ordercB_in_g(x1) = in_ordercB_in_g(x1)
in_ordercB_out_g(x1) = in_ordercB_out_g(x1)
U14_ag(x1, x2) = U14_ag(x1, x2)
U15_ag(x1, x2, x3, x4, x5) = U15_ag(x4, x5)
U16_ag(x1, x2, x3, x4, x5, x6, x7) = U16_ag(x2, x4, x6, x7)
U17_ag(x1, x2, x3, x4, x5) = U17_ag(x1, x2, x4, x5)
void = void
node(x1, x2, x3) = node(x1, x2, x3)
APPA_IN_AAAG(x1, x2, x3, x4) = APPA_IN_AAAG(x4)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPA_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPA_IN_AAAG(X2, X3, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
APPA_IN_AAAG(x1, x2, x3, x4) = APPA_IN_AAAG(x4)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPA_IN_AAAG(.(X1, X5)) → APPA_IN_AAAG(X5)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APPA_IN_AAAG(.(X1, X5)) → APPA_IN_AAAG(X5)
The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

IN_ORDERD_IN_AG(node(X1, X2, X3), X4) → U5_AG(X1, X2, X3, X4, appcF_in_aaag(X5, X2, X6, X4))
U5_AG(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X1, X5)
U5_AG(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U7_AG(X1, X2, X3, X4, X6, in_ordercD_in_ag(X1, X5))
U7_AG(X1, X2, X3, X4, X6, in_ordercD_out_ag(X1, X5)) → IN_ORDERD_IN_AG(X3, X6)

The TRS R consists of the following rules:

appcF_in_aaag([], X1, X2, .(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_in_aaag(X9, X10, X11, X12))
appcC_in_aaag([], X1, X2, .(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U11_aaag(X1, X2, X3, X4, X5, appcC_in_aaag(X2, X3, X4, X5))
U11_aaag(X1, X2, X3, X4, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
in_ordercD_in_ag(void, []) → in_ordercD_out_ag(void, [])
in_ordercD_in_ag(void, X1) → U12_ag(X1, appcE_in_aaag(X2, X3, X4, X1))
appcE_in_aaag([], X1, X2, .(X1, X2)) → appcE_out_aaag([], X1, X2, .(X1, X2))
appcE_in_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3))) → appcE_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcE_in_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4)))) → appcE_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcE_in_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5))))) → appcE_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_in_aaag(X9, X10, X11, X12))
appcA_in_aaag([], X1, X2, .(X1, X2)) → appcA_out_aaag([], X1, X2, .(X1, X2))
appcA_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U10_aaag(X1, X2, X3, X4, X5, appcA_in_aaag(X2, X3, X4, X5))
U10_aaag(X1, X2, X3, X4, X5, appcA_out_aaag(X2, X3, X4, X5)) → appcA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, appcA_out_aaag(X9, X10, X11, X12)) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U12_ag(X1, appcE_out_aaag(X2, X3, X4, X1)) → U13_ag(X1, X2, X3, X4, in_ordercB_in_g(X2))
in_ordercB_in_g([]) → in_ordercB_out_g([])
U13_ag(X1, X2, X3, X4, in_ordercB_out_g(X2)) → U14_ag(X1, in_ordercB_in_g(X4))
U14_ag(X1, in_ordercB_out_g(X4)) → in_ordercD_out_ag(void, X1)
in_ordercD_in_ag(node(X1, X2, X3), X4) → U15_ag(X1, X2, X3, X4, appcF_in_aaag(X5, X2, X6, X4))
U15_ag(X1, X2, X3, X4, appcF_out_aaag(X5, X2, X6, X4)) → U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_in_ag(X1, X5))
U16_ag(X1, X2, X3, X4, X5, X6, in_ordercD_out_ag(X1, X5)) → U17_ag(X1, X2, X3, X4, in_ordercD_in_ag(X3, X6))
U17_ag(X1, X2, X3, X4, in_ordercD_out_ag(X3, X6)) → in_ordercD_out_ag(node(X1, X2, X3), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
appcF_in_aaag(x1, x2, x3, x4) = appcF_in_aaag(x4)
appcF_out_aaag(x1, x2, x3, x4) = appcF_out_aaag(x1, x2, x3, x4)
U19_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U19_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x12, x13)
appcC_in_aaag(x1, x2, x3, x4) = appcC_in_aaag(x4)
appcC_out_aaag(x1, x2, x3, x4) = appcC_out_aaag(x1, x2, x3, x4)
U11_aaag(x1, x2, x3, x4, x5, x6) = U11_aaag(x1, x5, x6)
in_ordercD_in_ag(x1, x2) = in_ordercD_in_ag(x2)
[] = []
in_ordercD_out_ag(x1, x2) = in_ordercD_out_ag(x1, x2)
U12_ag(x1, x2) = U12_ag(x1, x2)
appcE_in_aaag(x1, x2, x3, x4) = appcE_in_aaag(x4)
appcE_out_aaag(x1, x2, x3, x4) = appcE_out_aaag(x1, x2, x3, x4)
U18_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U18_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x12, x13)
appcA_in_aaag(x1, x2, x3, x4) = appcA_in_aaag(x4)
appcA_out_aaag(x1, x2, x3, x4) = appcA_out_aaag(x1, x2, x3, x4)
U10_aaag(x1, x2, x3, x4, x5, x6) = U10_aaag(x1, x5, x6)
U13_ag(x1, x2, x3, x4, x5) = U13_ag(x1, x4, x5)
in_ordercB_in_g(x1) = in_ordercB_in_g(x1)
in_ordercB_out_g(x1) = in_ordercB_out_g(x1)
U14_ag(x1, x2) = U14_ag(x1, x2)
U15_ag(x1, x2, x3, x4, x5) = U15_ag(x4, x5)
U16_ag(x1, x2, x3, x4, x5, x6, x7) = U16_ag(x2, x4, x6, x7)
U17_ag(x1, x2, x3, x4, x5) = U17_ag(x1, x2, x4, x5)
void = void
node(x1, x2, x3) = node(x1, x2, x3)
IN_ORDERD_IN_AG(x1, x2) = IN_ORDERD_IN_AG(x2)
U5_AG(x1, x2, x3, x4, x5) = U5_AG(x4, x5)
U7_AG(x1, x2, x3, x4, x5, x6) = U7_AG(x4, x5, x6)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IN_ORDERD_IN_AG(X4) → U5_AG(X4, appcF_in_aaag(X4))
U5_AG(X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X5)
U5_AG(X4, appcF_out_aaag(X5, X2, X6, X4)) → U7_AG(X4, X6, in_ordercD_in_ag(X5))
U7_AG(X4, X6, in_ordercD_out_ag(X1, X5)) → IN_ORDERD_IN_AG(X6)

The TRS R consists of the following rules:

appcF_in_aaag(.(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_in_aaag(X12))
appcC_in_aaag(.(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, appcC_in_aaag(X5))
U11_aaag(X1, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
in_ordercD_in_ag([]) → in_ordercD_out_ag(void, [])
in_ordercD_in_ag(X1) → U12_ag(X1, appcE_in_aaag(X1))
appcE_in_aaag(.(X1, X2)) → appcE_out_aaag([], X1, X2, .(X1, X2))
appcE_in_aaag(.(X1, .(X2, X3))) → appcE_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcE_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcE_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcE_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcA_in_aaag(X12))
appcA_in_aaag(.(X1, X2)) → appcA_out_aaag([], X1, X2, .(X1, X2))
appcA_in_aaag(.(X1, X5)) → U10_aaag(X1, X5, appcA_in_aaag(X5))
U10_aaag(X1, X5, appcA_out_aaag(X2, X3, X4, X5)) → appcA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcA_out_aaag(X9, X10, X11, X12)) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U12_ag(X1, appcE_out_aaag(X2, X3, X4, X1)) → U13_ag(X1, X4, in_ordercB_in_g(X2))
in_ordercB_in_g([]) → in_ordercB_out_g([])
U13_ag(X1, X4, in_ordercB_out_g(X2)) → U14_ag(X1, in_ordercB_in_g(X4))
U14_ag(X1, in_ordercB_out_g(X4)) → in_ordercD_out_ag(void, X1)
in_ordercD_in_ag(X4) → U15_ag(X4, appcF_in_aaag(X4))
U15_ag(X4, appcF_out_aaag(X5, X2, X6, X4)) → U16_ag(X2, X4, X6, in_ordercD_in_ag(X5))
U16_ag(X2, X4, X6, in_ordercD_out_ag(X1, X5)) → U17_ag(X1, X2, X4, in_ordercD_in_ag(X6))
U17_ag(X1, X2, X4, in_ordercD_out_ag(X3, X6)) → in_ordercD_out_ag(node(X1, X2, X3), X4)

The set Q consists of the following terms:

appcF_in_aaag(x0)
appcC_in_aaag(x0)
U11_aaag(x0, x1, x2)
U19_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
in_ordercD_in_ag(x0)
appcE_in_aaag(x0)
appcA_in_aaag(x0)
U10_aaag(x0, x1, x2)
U18_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
U12_ag(x0, x1)
in_ordercB_in_g(x0)
U13_ag(x0, x1, x2)
U14_ag(x0, x1)
U15_ag(x0, x1)
U16_ag(x0, x1, x2, x3)
U17_ag(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

U7_AG(X4, X6, in_ordercD_out_ag(X1, X5)) → IN_ORDERD_IN_AG(X6)

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(IN_ORDERD_IN_AG(x₁)) = -I + 1A · x₁

POL(U5_AG(x₁, x₂)) = -I + 0A · x₁ + 0A · x₂

POL(appcF_in_aaag(x₁)) = -I + 1A · x₁

POL(appcF_out_aaag(x₁, x₂, x₃, x₄)) = 0A + 1A · x₁ + -I · x₂ + 2A · x₃ + -I · x₄

POL(U7_AG(x₁, x₂, x₃)) = -I + 0A · x₁ + 2A · x₂ + 0A · x₃

POL(in_ordercD_in_ag(x₁)) = 0A + 1A · x₁

POL(in_ordercD_out_ag(x₁, x₂)) = -I + 0A · x₁ + 0A · x₂

POL(.(x₁, x₂)) = 0A + -I · x₁ + 1A · x₂

POL([]) = 0A

POL(U19_aaag(x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉, x₁₀)) = 5A + -I · x₁ + -I · x₂ + -I · x₃ + -I · x₄ + -I · x₅ + -I · x₆ + -I · x₇ + -I · x₈ + 0A · x₉ + 5A · x₁₀

POL(appcC_in_aaag(x₁)) = -I + 4A · x₁

POL(void) = 0A

POL(U12_ag(x₁, x₂)) = 0A + 1A · x₁ + -I · x₂

POL(appcE_in_aaag(x₁)) = -I + 5A · x₁

POL(U15_ag(x₁, x₂)) = 0A + 1A · x₁ + -I · x₂

POL(U16_ag(x₁, x₂, x₃, x₄)) = 0A + -I · x₁ + 0A · x₂ + -I · x₃ + -I · x₄

POL(U17_ag(x₁, x₂, x₃, x₄)) = 0A + -I · x₁ + -I · x₂ + 0A · x₃ + -I · x₄

POL(node(x₁, x₂, x₃)) = 0A + -I · x₁ + -I · x₂ + -I · x₃

POL(appcC_out_aaag(x₁, x₂, x₃, x₄)) = 3A + 4A · x₁ + -I · x₂ + 5A · x₃ + -I · x₄

POL(U11_aaag(x₁, x₂, x₃)) = -I + -I · x₁ + -I · x₂ + 1A · x₃

POL(appcE_out_aaag(x₁, x₂, x₃, x₄)) = 0A + 5A · x₁ + 5A · x₂ + -I · x₃ + 1A · x₄

POL(U18_aaag(x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉, x₁₀)) = 0A + -I · x₁ + 0A · x₂ + 0A · x₃ + 0A · x₄ + -I · x₅ + -I · x₆ + 0A · x₇ + 0A · x₈ + -I · x₉ + -I · x₁₀

POL(appcA_in_aaag(x₁)) = -I + 0A · x₁

POL(U13_ag(x₁, x₂, x₃)) = 0A + 0A · x₁ + -I · x₂ + 0A · x₃

POL(in_ordercB_in_g(x₁)) = 0A + -I · x₁

POL(appcA_out_aaag(x₁, x₂, x₃, x₄)) = -I + 1A · x₁ + -I · x₂ + -I · x₃ + -I · x₄

POL(U10_aaag(x₁, x₂, x₃)) = 0A + 5A · x₁ + -I · x₂ + 0A · x₃

POL(in_ordercB_out_g(x₁)) = 0A + 0A · x₁

POL(U14_ag(x₁, x₂)) = 0A + 0A · x₁ + -I · x₂

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

appcF_in_aaag(.(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_in_aaag(X12))
in_ordercD_in_ag([]) → in_ordercD_out_ag(void, [])
in_ordercD_in_ag(X1) → U12_ag(X1, appcE_in_aaag(X1))
in_ordercD_in_ag(X4) → U15_ag(X4, appcF_in_aaag(X4))
U15_ag(X4, appcF_out_aaag(X5, X2, X6, X4)) → U16_ag(X2, X4, X6, in_ordercD_in_ag(X5))
U16_ag(X2, X4, X6, in_ordercD_out_ag(X1, X5)) → U17_ag(X1, X2, X4, in_ordercD_in_ag(X6))
U17_ag(X1, X2, X4, in_ordercD_out_ag(X3, X6)) → in_ordercD_out_ag(node(X1, X2, X3), X4)
appcC_in_aaag(.(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, appcC_in_aaag(X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U11_aaag(X1, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U12_ag(X1, appcE_out_aaag(X2, X3, X4, X1)) → U13_ag(X1, X4, in_ordercB_in_g(X2))
in_ordercB_in_g([]) → in_ordercB_out_g([])
U13_ag(X1, X4, in_ordercB_out_g(X2)) → U14_ag(X1, in_ordercB_in_g(X4))
U14_ag(X1, in_ordercB_out_g(X4)) → in_ordercD_out_ag(void, X1)

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IN_ORDERD_IN_AG(X4) → U5_AG(X4, appcF_in_aaag(X4))
U5_AG(X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X5)
U5_AG(X4, appcF_out_aaag(X5, X2, X6, X4)) → U7_AG(X4, X6, in_ordercD_in_ag(X5))

The TRS R consists of the following rules:

appcF_in_aaag(.(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_in_aaag(X12))
appcC_in_aaag(.(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, appcC_in_aaag(X5))
U11_aaag(X1, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
in_ordercD_in_ag([]) → in_ordercD_out_ag(void, [])
in_ordercD_in_ag(X1) → U12_ag(X1, appcE_in_aaag(X1))
appcE_in_aaag(.(X1, X2)) → appcE_out_aaag([], X1, X2, .(X1, X2))
appcE_in_aaag(.(X1, .(X2, X3))) → appcE_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcE_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcE_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcE_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcA_in_aaag(X12))
appcA_in_aaag(.(X1, X2)) → appcA_out_aaag([], X1, X2, .(X1, X2))
appcA_in_aaag(.(X1, X5)) → U10_aaag(X1, X5, appcA_in_aaag(X5))
U10_aaag(X1, X5, appcA_out_aaag(X2, X3, X4, X5)) → appcA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcA_out_aaag(X9, X10, X11, X12)) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U12_ag(X1, appcE_out_aaag(X2, X3, X4, X1)) → U13_ag(X1, X4, in_ordercB_in_g(X2))
in_ordercB_in_g([]) → in_ordercB_out_g([])
U13_ag(X1, X4, in_ordercB_out_g(X2)) → U14_ag(X1, in_ordercB_in_g(X4))
U14_ag(X1, in_ordercB_out_g(X4)) → in_ordercD_out_ag(void, X1)
in_ordercD_in_ag(X4) → U15_ag(X4, appcF_in_aaag(X4))
U15_ag(X4, appcF_out_aaag(X5, X2, X6, X4)) → U16_ag(X2, X4, X6, in_ordercD_in_ag(X5))
U16_ag(X2, X4, X6, in_ordercD_out_ag(X1, X5)) → U17_ag(X1, X2, X4, in_ordercD_in_ag(X6))
U17_ag(X1, X2, X4, in_ordercD_out_ag(X3, X6)) → in_ordercD_out_ag(node(X1, X2, X3), X4)

The set Q consists of the following terms:

appcF_in_aaag(x0)
appcC_in_aaag(x0)
U11_aaag(x0, x1, x2)
U19_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
in_ordercD_in_ag(x0)
appcE_in_aaag(x0)
appcA_in_aaag(x0)
U10_aaag(x0, x1, x2)
U18_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
U12_ag(x0, x1)
in_ordercB_in_g(x0)
U13_ag(x0, x1, x2)
U14_ag(x0, x1)
U15_ag(x0, x1)
U16_ag(x0, x1, x2, x3)
U17_ag(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_AG(X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X5)
IN_ORDERD_IN_AG(X4) → U5_AG(X4, appcF_in_aaag(X4))

The TRS R consists of the following rules:

appcF_in_aaag(.(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_in_aaag(X12))
appcC_in_aaag(.(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, appcC_in_aaag(X5))
U11_aaag(X1, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
in_ordercD_in_ag([]) → in_ordercD_out_ag(void, [])
in_ordercD_in_ag(X1) → U12_ag(X1, appcE_in_aaag(X1))
appcE_in_aaag(.(X1, X2)) → appcE_out_aaag([], X1, X2, .(X1, X2))
appcE_in_aaag(.(X1, .(X2, X3))) → appcE_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcE_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcE_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcE_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcE_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcA_in_aaag(X12))
appcA_in_aaag(.(X1, X2)) → appcA_out_aaag([], X1, X2, .(X1, X2))
appcA_in_aaag(.(X1, X5)) → U10_aaag(X1, X5, appcA_in_aaag(X5))
U10_aaag(X1, X5, appcA_out_aaag(X2, X3, X4, X5)) → appcA_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
U18_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcA_out_aaag(X9, X10, X11, X12)) → appcE_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U12_ag(X1, appcE_out_aaag(X2, X3, X4, X1)) → U13_ag(X1, X4, in_ordercB_in_g(X2))
in_ordercB_in_g([]) → in_ordercB_out_g([])
U13_ag(X1, X4, in_ordercB_out_g(X2)) → U14_ag(X1, in_ordercB_in_g(X4))
U14_ag(X1, in_ordercB_out_g(X4)) → in_ordercD_out_ag(void, X1)
in_ordercD_in_ag(X4) → U15_ag(X4, appcF_in_aaag(X4))
U15_ag(X4, appcF_out_aaag(X5, X2, X6, X4)) → U16_ag(X2, X4, X6, in_ordercD_in_ag(X5))
U16_ag(X2, X4, X6, in_ordercD_out_ag(X1, X5)) → U17_ag(X1, X2, X4, in_ordercD_in_ag(X6))
U17_ag(X1, X2, X4, in_ordercD_out_ag(X3, X6)) → in_ordercD_out_ag(node(X1, X2, X3), X4)

The set Q consists of the following terms:

appcF_in_aaag(x0)
appcC_in_aaag(x0)
U11_aaag(x0, x1, x2)
U19_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
in_ordercD_in_ag(x0)
appcE_in_aaag(x0)
appcA_in_aaag(x0)
U10_aaag(x0, x1, x2)
U18_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
U12_ag(x0, x1)
in_ordercB_in_g(x0)
U13_ag(x0, x1, x2)
U14_ag(x0, x1)
U15_ag(x0, x1)
U16_ag(x0, x1, x2, x3)
U17_ag(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(30) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_AG(X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X5)
IN_ORDERD_IN_AG(X4) → U5_AG(X4, appcF_in_aaag(X4))

The TRS R consists of the following rules:

appcF_in_aaag(.(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_in_aaag(X12))
appcC_in_aaag(.(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, appcC_in_aaag(X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U11_aaag(X1, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))

The set Q consists of the following terms:

appcF_in_aaag(x0)
appcC_in_aaag(x0)
U11_aaag(x0, x1, x2)
U19_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
in_ordercD_in_ag(x0)
appcE_in_aaag(x0)
appcA_in_aaag(x0)
U10_aaag(x0, x1, x2)
U18_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
U12_ag(x0, x1)
in_ordercB_in_g(x0)
U13_ag(x0, x1, x2)
U14_ag(x0, x1)
U15_ag(x0, x1)
U16_ag(x0, x1, x2, x3)
U17_ag(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(32) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

in_ordercD_in_ag(x0)
appcE_in_aaag(x0)
appcA_in_aaag(x0)
U10_aaag(x0, x1, x2)
U18_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)
U12_ag(x0, x1)
in_ordercB_in_g(x0)
U13_ag(x0, x1, x2)
U14_ag(x0, x1)
U15_ag(x0, x1)
U16_ag(x0, x1, x2, x3)
U17_ag(x0, x1, x2, x3)

(33) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_AG(X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X5)
IN_ORDERD_IN_AG(X4) → U5_AG(X4, appcF_in_aaag(X4))

The TRS R consists of the following rules:

appcF_in_aaag(.(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))
appcF_in_aaag(.(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_in_aaag(X12))
appcC_in_aaag(.(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, appcC_in_aaag(X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U11_aaag(X1, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))

The set Q consists of the following terms:

appcF_in_aaag(x0)
appcC_in_aaag(x0)
U11_aaag(x0, x1, x2)
U19_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)

We have to consider all (P,Q,R)-chains.

(34) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

appcF_in_aaag(.(X1, X2)) → appcF_out_aaag([], X1, X2, .(X1, X2))

Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 2
POL(IN_ORDERD_IN_AG(x₁)) = 2·x₁
POL(U11_aaag(x₁, x₂, x₃)) = 1
POL(U19_aaag(x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉, x₁₀)) = 2
POL(U5_AG(x₁, x₂)) = 2·x₂
POL([]) = 0
POL(appcC_in_aaag(x₁)) = 1
POL(appcC_out_aaag(x₁, x₂, x₃, x₄)) = 1
POL(appcF_in_aaag(x₁)) = x₁
POL(appcF_out_aaag(x₁, x₂, x₃, x₄)) = x₁

(35) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_AG(X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X5)
IN_ORDERD_IN_AG(X4) → U5_AG(X4, appcF_in_aaag(X4))

The TRS R consists of the following rules:

appcF_in_aaag(.(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_in_aaag(X12))
appcC_in_aaag(.(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, appcC_in_aaag(X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U11_aaag(X1, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))

The set Q consists of the following terms:

appcF_in_aaag(x0)
appcC_in_aaag(x0)
U11_aaag(x0, x1, x2)
U19_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)

We have to consider all (P,Q,R)-chains.

(36) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

U5_AG(X4, appcF_out_aaag(X5, X2, X6, X4)) → IN_ORDERD_IN_AG(X5)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:

POL(.(x₁, x₂)) = [1/4] + x₂
POL(IN_ORDERD_IN_AG(x₁)) = [1/4] + [1/4]x₁
POL(U11_aaag(x₁, x₂, x₃)) = [1] + x₃
POL(U19_aaag(x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉, x₁₀)) = [2] + [1/4]x₁₀
POL(U5_AG(x₁, x₂)) = [1/4] + [1/4]x₂
POL([]) = 0
POL(appcC_in_aaag(x₁)) = [4]x₁
POL(appcC_out_aaag(x₁, x₂, x₃, x₄)) = [1] + [4]x₁ + [2]x₃
POL(appcF_in_aaag(x₁)) = x₁
POL(appcF_out_aaag(x₁, x₂, x₃, x₄)) = [1/4] + x₁ + [1/4]x₃

The value of delta used in the strict ordering is 1/16.
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

appcF_in_aaag(.(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_in_aaag(X12))
appcC_in_aaag(.(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, appcC_in_aaag(X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U11_aaag(X1, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))

(37) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IN_ORDERD_IN_AG(X4) → U5_AG(X4, appcF_in_aaag(X4))

The TRS R consists of the following rules:

appcF_in_aaag(.(X1, .(X2, X3))) → appcF_out_aaag(.(X1, []), X2, X3, .(X1, .(X2, X3)))
appcF_in_aaag(.(X1, .(X2, .(X3, X4)))) → appcF_out_aaag(.(X1, .(X2, [])), X3, X4, .(X1, .(X2, .(X3, X4))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, X5))))) → appcF_out_aaag(.(X1, .(X2, .(X3, []))), X4, X5, .(X1, .(X2, .(X3, .(X4, X5)))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, X6)))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, [])))), X5, X6, .(X1, .(X2, .(X3, .(X4, .(X5, X6))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, []))))), X6, X7, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, X7)))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8)))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, [])))))), X7, X8, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, X8))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9))))))))) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, []))))))), X8, X9, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))))
appcF_in_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12))))))))) → U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_in_aaag(X12))
appcC_in_aaag(.(X1, X2)) → appcC_out_aaag([], X1, X2, .(X1, X2))
appcC_in_aaag(.(X1, X5)) → U11_aaag(X1, X5, appcC_in_aaag(X5))
U19_aaag(X1, X2, X3, X4, X5, X6, X7, X8, X12, appcC_out_aaag(X9, X10, X11, X12)) → appcF_out_aaag(.(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X9)))))))), X10, X11, .(X1, .(X2, .(X3, .(X4, .(X5, .(X6, .(X7, .(X8, X12)))))))))
U11_aaag(X1, X5, appcC_out_aaag(X2, X3, X4, X5)) → appcC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))

The set Q consists of the following terms:

appcF_in_aaag(x0)
appcC_in_aaag(x0)
U11_aaag(x0, x1, x2)
U19_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9)

We have to consider all (P,Q,R)-chains.

(38) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

(4) Obligation:

(5) TriplesToPiDPProof (SOUND transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) Obligation:

(30) UsableRulesProof (EQUIVALENT transformation)

(31) Obligation:

(32) QReductionProof (EQUIVALENT transformation)

(33) Obligation:

(34) QDPQMonotonicMRRProof (EQUIVALENT transformation)

(35) Obligation:

(36) QDPOrderProof (EQUIVALENT transformation)

(37) Obligation:

(38) DependencyGraphProof (EQUIVALENT transformation)

(39) TRUE